COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	hyperc[w82,jmc]		Hyperconsistency we sometimes need more than consistency
C00008 ENDMK
C⊗;
hyperc[w82,jmc]		Hyperconsistency; we sometimes need more than consistency

	First order logic is easily proved consistent.  The usual proofs
of consistency involve showing that the axioms are satisfied in
a domain of one element and that the rules of inference preserve
satisfaction in a domain of one element.  However, the mere fact that
first order logic is consistent doesn't tell us that it remains consistent
when we adjoin the sentence

P(a) ∧ ¬P(b)

which requires a domain of at least two elements for its satisfaction.
Therefore, we would like something stronger than a mere consistency theorem,
but it isn't clear exactly what is wanted.  However, we need to know that
the system remains consistent when certain "harmless" collections of
sentences are added.

	Let us consider two examples.

	1. The blocks world.  The predicates are  on(x,y)  and  above(x,y),
and we have axioms and schemata asserting that  above  is the transitive closure
of  on.  We also have an axiom asserting that no block is above itself.
  These are the general axioms, and they are easily seen to be
consistent by taking an example where there is just one block.  Indeed if
some other objects exist, the simplest model is where there are no blocks
at all.

	Now consider a particular "blocks situation" axiomatized by a
collection of ground assertions of the form  on(a,b) and of the form ¬on(c,d),
where the  a's, b's, c's and d's are individual constants.  Such an
axiomatization is not necessarily consistent, because it may imply
that some block is above itself.

	However, suppose we have a finite collection  A  of such axioms,
each a ground assertion and involving a collection  I(A)  of individual
constants.  Suppose  A  is purported to describe a blocks situation.
We would like a way of testing whether it is satisfiable.  Of course,
if the axioms are propositionally inconsistent, there will be no
model.  However, the single axioms  on(A,A)  is propositionally consistent
and so is the more elaborate collection {on(A,B),on(B,C),on(C,A)}.  However,
neither has a model satisfying the general blocks axioms.

	Now suppose we adjoin to the collection  A  all instances of
the general axioms where the variables instantiated by elements of  D1.
This is a finite collection of sentences  A'.  We assert that the axiom
system is consistent as a whole provided  A'  is propositionally consistent.
This seems apparent, because the only thing that can apparently go wrong
is that there can be some finite cycles of  on's leading to a block being
above itself.  However, we don't have a proof of this fact.

	2. Axioms about knowledge.  Axiom systems for knowledge are
complex, and it sometimes isn't obvious whether they are consistent.
A fortiori, it may not be obvious whether they such a system remains
consistent when an apparently harmless description of a particular
situation is adjoined.  We would like hyperconsistency theorems like
that conjectured above for the blocks world.  Namely, a finite collection  A
of assertions may be consistently adjoined to the knowledge axioms
provided a certain expanded finite collection  A'  is propositionally consistent.